A,B:es_realizer{i:l}.
(i:Id. ((R-has-loc(A; i))  (R-has-loc(B; i))))  R-icompat(A; B)  R-compat{i:l}(A; B) 

latex

Definitions

T, P  Q, P  Q, guard(T), P  Q, ff, tt, if b then t else f fi , ge(i; j), False, A  B, True, Y, prop{i:l}, t  T, R-compat{i:l}(A; B), R-icompat(A; B), P  Q, A, P  Q, x:A. B(x), Unit, , , ,

Lemmas

R-has-loc-base, squash wf, not functionality wrt iff, assert-eq-id, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, ge wf, nat properties, R-loc wf, eq id wf, true wf, Rnone? wf, bnot wf, Rplus-right wf, assert of bor, R-has-loc-Rplus, Rplus-left wf, R-size-decreases, bool wf, Rplus? wf, le wf, es realizer wf, R-has-loc wf, assert wf, not wf, Id wf, R-icompat wf, nat plus wf, R-size wf, nat wf